(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_BV)
(declare-fun v0 () (_ BitVec 16))
(declare-fun v1 () (_ BitVec 13))
(declare-fun v2 () (_ BitVec 2))
(assert (let ((e3(_ bv202 9)))
(let ((e4 (bvmul v0 ((_ sign_extend 7) e3))))
(let ((e5 (bvnand ((_ zero_extend 3) v1) v0)))
(let ((e6 (ite (bvult v0 v0) (_ bv1 1) (_ bv0 1))))
(let ((e7 (bvsdiv ((_ sign_extend 14) v2) e4)))
(let ((e8 (bvuge v0 ((_ zero_extend 3) v1))))
(let ((e9 (bvslt e4 ((_ zero_extend 15) e6))))
(let ((e10 (bvuge e5 e5)))
(let ((e11 (bvult ((_ sign_extend 14) v2) e4)))
(let ((e12 (= ((_ sign_extend 11) v2) v1)))
(let ((e13 (bvult e7 ((_ sign_extend 14) v2))))
(let ((e14 (bvuge e5 ((_ zero_extend 3) v1))))
(let ((e15 (bvult ((_ sign_extend 11) v2) v1)))
(let ((e16 (bvsle ((_ zero_extend 4) e3) v1)))
(let ((e17 (ite e13 e14 e9)))
(let ((e18 (and e8 e10)))
(let ((e19 (or e16 e15)))
(let ((e20 (ite e19 e18 e19)))
(let ((e21 (ite e11 e11 e17)))
(let ((e22 (ite e21 e12 e21)))
(let ((e23 (and e22 e20)))
(let ((e24 (and e23 (not (= e4 (_ bv0 16))))))
(let ((e25 (and e24 (not (= e4 (bvnot (_ bv0 16)))))))
e25
))))))))))))))))))))))))

;; CHECK: (assert (= v0 (_ bv17660 16)))
;; CHECK: (check-sat)
(check-sat-assuming-model (v0) ((_ bv17660 16)))
